Nuprl Lemma : R-possible-Rplus
11,40
postcript
pdf
A
,
B
:Realizer,
es
:ES. Possible(
A
B
;
es
)
{Possible(
A
;
es
) & Possible(
B
;
es
) &
A
||
B
}
latex
Definitions
,
t
T
,
Top
,
x
:
A
.
B
(
x
)
,
A
c
B
,
P
&
Q
,
{
T
}
,
Possible(
R
;
es
)
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
es
realizer
wf
,
event
system
wf
,
Rplus
wf
,
R-possible
wf
,
R-compat-implies
,
dsys-sub-join-right
,
fair-fifo
wf
,
w-es
wf
,
possible-world
wf
,
dsys-sub-join-left
,
R-Dsys-Rplus
,
R-Dsys
wf
,
possible-world-monotonic
,
R-Feasible-Rplus
origin
A, B:Realizer, es:ES. Possible(A 
B;es) 
{Possible(A;es) & Possible(B;es) & A || B} A, B:Realizer, es:ES. Possible(A B;es) {Possible(A;es) & Possible(B;es) & A || B} 
T
x:A. B(x)
B